f:top, T:Type, L:(T List), i:int_seg(0; ||L||). sqequal(map(f; L)[i]; (f(L[i]))) 

latex

Definitions	x:A. B(x), ||as||, map(f; as), Y, t  T, l[i], sq_type(T), P  Q, guard(T), prop{i:l}, hd(l), nth_tl(n;as), if b then t else f fi , i z j, b, i <z j, tt, ff, tl(l), P  Q, P  Q, P  Q, T, True, int_seg(i; j), A, lelt(i; j; k), A  B, False, decidable(P), P  Q, , Unit,
Lemmas	int seg wf, length wf1, top wf, decidable int equal, le int wf, bool wf, iff transitivity, assert wf, le wf, eqtt to assert, assert of le int, lt int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int